SAT 问题

概述

布尔可满足性问题（SAT）是计算复杂度理论中最核心的问题之一：给定一个布尔公式，判断是否存在一组变量赋值使得公式为真。1971年被 Cook 证明为第一个 NP 完全问题。

关键内容

问题定义

给定一个布尔公式 φ（由变量 x₁, x₂, ..., xₙ、逻辑连接词 ∧（与）、∨（或）、¬（非）组成），判断是否存在一组变量赋值（每个变量取 TRUE 或 FALSE），使得 φ 的值为 TRUE。

示例： - (x₁ ∨ ¬x₂) ∧ (¬x₁ ∨ x₃) 是可满足的（取 x₁=TRUE, x₂=FALSE, x₃=TRUE） - x₁ ∧ ¬x₁ 是不可满足的

CNF-SAT

Cook 证明了即使是合取范式（CNF）形式的 SAT 也是 NP 完全的：公式是若干子句的合取，每个子句是若干文字的析取。

Cook-Levin 定理

Cook（1971）和 Levin（1973）独立证明了 SAT 是 NP 完全的——任何 NP 问题都可以在多项式时间内归约到 SAT。

现代 SAT 求解器

尽管 SAT 是 NP 完全的，现代 SAT 求解器取得了惊人的实际性能： - CDCL 算法（Conflict-Driven Clause Learning）：MiniSat、CaDiCaL、Kissat - 可以在合理时间内求解包含数百万变量和数千万子句的工业级实例 - 应用于硬件验证、软件测试、人工智能规划等领域

这并不与 NP 完全性矛盾——工业级 SAT 实例通常具有特殊结构（如社区结构、变量间的局部依赖关系），使得求解器可以避免最坏情况。

来源

raw/books/计算机科学/08-cook-np-completeness.md